Skip to content

List Subcommand (Implementation)#3523

Merged
carolynzech merged 40 commits into
model-checking:mainfrom
carolynzech:list-subcommand
Oct 9, 2024
Merged

List Subcommand (Implementation)#3523
carolynzech merged 40 commits into
model-checking:mainfrom
carolynzech:list-subcommand

Conversation

@carolynzech

@carolynzech carolynzech commented Sep 17, 2024 •
edited
Loading

Copy link
Copy Markdown
Contributor

Implementation of the list subcommand (and updates to the RFC).

As a larger test, I ran on the standard library (kani list -Z list -Z function-contracts -Z mem-predicates ./library --std) and manually verified that the results were correct. I pasted the output below.

Contracts:

Function Contract Harnesses (#[kani::proof_for_contract])
alloc::layout::Layout::from_size_align_unchecked alloc::layout::verify::check_from_size_align_unchecked
ascii::ascii_char::AsciiChar::from_u8 ascii::ascii_char::verify::check_from_u8
ascii::ascii_char::AsciiChar::from_u8_unchecked ascii::ascii_char::verify::check_from_u8_unchecked
char::convert::from_u32_unchecked char::convert::verify::check_from_u32_unchecked
char::methods::verify::as_ascii_clone char::methods::verify::check_as_ascii_ascii_char
char::methods::verify::check_as_ascii_non_ascii_char
intrinsics::typed_swap intrinsics::verify::check_typed_swap_u8
intrinsics::verify::check_typed_swap_char
intrinsics::verify::check_typed_swap_non_zero
mem::swap mem::verify::check_swap_primitive
mem::verify::check_swap_adt_no_drop
ptr::align_offset ptr::verify::check_align_offset_zst
ptr::verify::check_align_offset_u8
ptr::verify::check_align_offset_u16
ptr::verify::check_align_offset_u32
ptr::verify::check_align_offset_u64
ptr::verify::check_align_offset_u128
ptr::verify::check_align_offset_4096
ptr::verify::check_align_offset_5
ptr::alignment::Alignment::as_nonzero ptr::alignment::verify::check_as_nonzero
ptr::alignment::Alignment::as_usize ptr::alignment::verify::check_as_usize
ptr::alignment::Alignment::log2 ptr::alignment::verify::check_log2
ptr::alignment::Alignment::mask ptr::alignment::verify::check_mask
ptr::alignment::Alignment::new ptr::alignment::verify::check_new
ptr::alignment::Alignment::new_unchecked ptr::alignment::verify::check_new_unchecked
ptr::alignment::Alignment::of ptr::alignment::verify::check_of_i32
ptr::non_null::NonNull::::new ptr::non_null::verify::non_null_check_new
ptr::non_null::NonNull::::new_unchecked ptr::non_null::verify::non_null_check_new_unchecked
ptr::read_volatile ptr::verify::check_read_u128
ptr::unique::Unique::::as_non_null_ptr ptr::unique::verify::check_as_non_null_ptr
ptr::unique::Unique::::as_ptr ptr::unique::verify::check_as_ptr
ptr::unique::Unique::::new ptr::unique::verify::check_new
ptr::unique::Unique::::new_unchecked ptr::unique::verify::check_new_unchecked
ptr::verify::mod_inv_copy ptr::verify::check_mod_inv
ptr::write_volatile NONE
Total 24 34

Standard Harnesses (#[kani::proof]):

  1. ptr::unique::verify::check_as_mut
  2. ptr::unique::verify::check_as_ref
  3. ptr::unique::verify::check_cast

Terminal view (--pretty format):
list

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

Loading
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@feliperodri feliperodri feliperodri approved these changes

@jaisnan jaisnan Awaiting requested review from jaisnan

+3 more reviewers

@camshaft camshaft camshaft left review comments

@celinval celinval celinval left review comments

@zhassan-aws zhassan-aws zhassan-aws approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

@carolynzech carolynzech

Labels

Z-EndToEndBenchCI Tag a PR to run benchmark CI

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@carolynzech @celinval @camshaft @feliperodri @zhassan-aws